Nuprl Lemma : map_is_nil
0,22
postcript
pdf
A
,
B
:Type,
f
:(
A
B
),
l
:
A
List. map(
f
;
l
) = nil
B
List
l
= nil
latex
Definitions
Y
,
map(
f
;
as
)
,
t
T
,
Prop
,
P
Q
,
x
:
A
.
B
(
x
)
,
P
Q
,
P
&
Q
,
P
Q
,
False
Lemmas
map
wf
origin
A, B:Type, f:(A
B), l:A List. map(f;l) = nil 
B List 
l = nil A, B:Type, f:(AB), l:A List. map(f;l) = nil B List l = nil T
Qx:A. B(x) Q Q